Skip to content

mbp: term: Fix reorder ctor warning.#7016

Merged
NikolajBjorner merged 1 commit intoZ3Prover:masterfrom
waywardmonkeys:fix-reorder-ctor-warning
Nov 26, 2023
Merged

mbp: term: Fix reorder ctor warning.#7016
NikolajBjorner merged 1 commit intoZ3Prover:masterfrom
waywardmonkeys:fix-reorder-ctor-warning

Conversation

@waywardmonkeys
Copy link
Contributor

Initialize members in same order they are defined.

Initialize members in same order they are defined.
@NikolajBjorner NikolajBjorner merged commit b5e8f59 into Z3Prover:master Nov 26, 2023
@waywardmonkeys waywardmonkeys deleted the fix-reorder-ctor-warning branch November 27, 2023 06:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants